(DEFUN NEWSUBLIS (P E) 
       (COND ((ATOM E)
	      ((LAMBDA (Z) (COND ((NULL Z) E) (T (CDR Z))))
	       (ASSOC E P)))
	     ((ISQUANT (CAR E))
	      (CONS (CAR E)
		    (NEWSUBLIS (APPEND P (NEWPAIRS (CADR E)))
			       (CDR E))))
	     (T (CONS (NEWSUBLIS P (CAR E)) (NEWSUBLIS P (CDR E)))))) 

(DEFUN ISQUANT (SYM) (MEMBER SYM '(ALL EXIST LAMBDA))) 

(DEFUN NEWPAIRS (U) 
       (COND ((NULL U) NIL)
	     (T (CONS (CONS (CAR U) (GENSYM)) (NEWPAIRS (CDR U))))))